

(*       ___                                                              *)
(*      ||M||                                                             *)
(*      ||A||       A project by Andrea Asperti                           *)
(*      ||T||                                                             *)
(*      ||I||       Developers:                                           *)
(*      ||T||         The HELM team.                                      *)
(*      ||A||         http://helm.cs.unibo.it                             *)
(*      \   /                                                             *)
(*       \ /        This file is distributed under the terms of the       *)
(*        v         GNU General Public License Version 2                  *)
(*                                                                        *)
(**************************************************************************)
include "formulas.ma".
include "setoids.ma".

(*** Relation on formulas ***)
inductive RelFormula : Formula → Formula → Prop ≝ 
(* De Morgan laws *) 
| RelFormulaNegOne  :        RelFormula (Neg One        )  One
| RelFormulaNegAtom : ∀ n  . RelFormula (Neg ( Atom n  )) (NAtom n)
| RelFormulaNegNAtom: ∀ n  . RelFormula (Neg (NAtom n  )) ( Atom n)
| RelFormulaNegTimes: ∀ R,T. RelFormula (Neg (Times R T)) (Par   (Neg R) (Neg T))
| RelFormulaNegPar  : ∀ R,T. RelFormula (Neg (Par   R T)) (Times (Neg R) (Neg T))
(* Unit laws *) 
| RelFormulaParUnit: ∀ R. RelFormula (𝟙 ⊠ R) R
| RelFormulaCopUnit: ∀ R. RelFormula (𝟙 ⊗ R) R
(* Associativity from left to right *)
| RelFormulaParAsc: ∀ R,T,U. RelFormula (R ⊠ (T ⊠ U)) (R ⊠ T ⊠ U) 
| RelFormulaCopAsc: ∀ R,T,U. RelFormula (R ⊗ (T ⊗ U)) (R ⊗ T ⊗ U) 
(* Symmetry *)
| RelFormulaParSym: ∀ R,T. RelFormula (R ⊠ T) (T ⊠ R)
| RelFormulaCopSym: ∀ R,T. RelFormula (R ⊗ T) (T ⊗ R)
(* Inverse *)
| RelFormulaComm  : ∀ R,T. RelFormula T R →  RelFormula R T .

(*** Contextual closure of RelFormulas ***)
inductive CntFormula : Formula → Formula → Prop ≝ 
| CntFormulaLift: ∀ R,T  . RelFormula R T → CntFormula R T
| CntFormulaNeg : ∀ R,T  . CntFormula R T → CntFormula (Neg R) (Neg T)
| CntFormulaParL: ∀ R,T,U. CntFormula R T → CntFormula (R ⊠ U) (T ⊠ U)
| CntFormulaParR: ∀ R,T,U. CntFormula R T → CntFormula (U ⊠ R) (U ⊠ T) 
| CntFormulaCopL: ∀ R,T,U. CntFormula R T → CntFormula (R ⊗ U) (T ⊗ U)
| CntFormulaCopR: ∀ R,T,U. CntFormula R T → CntFormula (U ⊗ R) (U ⊗ T) .



(* Reflexive and transitive closure of EqFormula. *)
inductive EqFormula : Formula → Formula → Prop ≝
| EqFormulaRefl: ∀ R    . EqFormula  R R
| EqFormulaLift: ∀ R,T  . CntFormula R T → EqFormula R T
| EqFormulaTran: ∀ R,U,T. EqFormula  R U → EqFormula U T → EqFormula R T .

(******* EqFormula is an equivalence relation START *******)
lemma EqFormula_is_Refl: ∀R. EqFormula R R.
// qed.

lemma EqFormula_is_Sym: ∀R,T.EqFormula R T → EqFormula T R.
  #F1 #F2 #R
 (* Discharging the assumptions. *)

 (* Proceeding by induction on the definition of H. *)
 elim R; 
 (* Since we have considered the different forms
    H can assume, the assumption H is useless. *)
 -R;
 [1: @EqFormulaRefl
 |2: #F3 #F4 #CNT @EqFormulaLift; elim CNT /2/ #F5 #F6 #Rel @CntFormulaLift /2/
 |3: #F3 #F4 #F5 #Eq1 #Eq2 #Eq3 #Eq4 /2/ ] qed.

lemma EqFormula_is_Tran: ∀R,U,T.EqFormula R U → EqFormula U T → EqFormula R T.
 /2/ qed.

definition EqRelFormula: equivalence_relation Formula.
 % 1;
 [1: (* Relation *)
     @EqFormula         (* which is: *)
 |2: @EqFormula_is_Refl (* reflexive, *)
 |3: @EqFormula_is_Sym (* symmetric, *)
 |4: @EqFormula_is_Tran (* transitive.*) ] qed.

notation "hvbox(a break ≃ b)" 
  non associative with precedence 45 
  for @{ 'EqRelFormula $a $b }.
interpretation "EqRelFormula" 'EqRelFormula x y = (EqRelFormula x y) .
(******* EqFormula is an equivalence relation STOP  *******)

(******* EqRelFormula is a congruence START *******)
lemma EqRelFormula_is_Refl: ∀ R. R ≃ R.
  #F whd @EqFormula_is_Refl qed.

lemma EqRelFormula_is_Sym: ∀ R,T. R ≃ T → T ≃ R.
  #F1 #F2 #Eq @(EqFormula_is_Sym) assumption qed.

lemma EqRelFormula_is_Tran:
   ∀ R,U,T. T ≃ U → U ≃ R → T ≃ R. /2/ qed.


lemma EqRelFormula_is_CntNeg: ∀ R,T. R ≃ T → R^⊥ ≃ T^⊥.
  #F1 #F2 #Eq elim Eq -Eq  
  [1,2:
    whd [ #F3 whd % | #F3 #F4 #Cnt whd @EqFormulaLift  /2/]
  |3: #F3 #F4 #F5 #Eq1 #Eq2 #EqRel1 #EqRel2 whd  /2/] qed.

lemma EqRelFormula_is_CntCopR: ∀ R,T,U. R ≃ T → (U ⊗ R) ≃ (U ⊗ T).
  #F1 #F2 #F3 #Eq
  whd in Eq; elim Eq -Eq
  [ #F4 whd @(EqFormula_is_Refl ?) 
  | #F4 #F5 #Cnt  whd; @EqFormulaLift /2/
  | #F4 #F5 #F6 #Eq1 #Eq2 #EqRel1 #EqRel2 whd whd in EqRel1 EqRel2;
   @(EqFormulaTran ? (F3 ⊗ F5) ?) //] qed.
   
lemma EqRelFormula_is_CntCopL: ∀ R,T,U. R ≃ T → (R ⊗ U)≃ (T ⊗ U).
  #F1 #F2 #F3 #EqRel
  whd in EqRel; whd elim EqRel -EqRel #F4
  /2/ #F5 #Cnt @EqFormulaLift @CntFormulaCopL assumption qed. 

lemma EqRelFormula_is_CntParR: ∀ R,T,U. R ≃ T → (U ⊠ R) ≃ (U ⊠ T).
  #F1 #F2 #F3 #EqRel
  whd in EqRel; whd elim EqRel -EqRel #F4 
  /2/ #F5 #Cnt @EqFormulaLift @CntFormulaParR assumption qed.
  
lemma EqRelFormula_is_CntParL: ∀ R,T,U. R ≃ T → (R ⊠ U) ≃ (T ⊠ U).
  #F1 #F2 #F3 #EqRel
  whd in EqRel; whd elim EqRel -EqRel #F4
  /2/  #F5 #Cnt @EqFormulaLift @CntFormulaParL assumption qed.  

lemma EqRelFormula_is_CntParLR: ∀ R,T,U,V. R ≃ T → U ≃ V → (R ⊠ U) ≃ (T ⊠ V).
  #F1 #F2 #F3 #F4 #EqRel1 #EqRel2
  @(EqRelFormula_is_Tran ?  (F1⊠F4) ?)
  /2/ qed.
   
lemma EqRelFormula_is_CntCopLR: ∀ R,T,U,V. R ≃ T → U ≃ V → (R ⊗ U) ≃ (T ⊗ V).
  #F1 #F2 #F3 #F4 #EqRel1 #EqRel2  
  @(EqRelFormula_is_Tran ? (F1 ⊗ F4) ?)
  /2/ qed.
(******* EqRelFormula is a congruence STOP  *******)

(******  F^⊥^⊥ ≈ F ⇔ (∃G.G^⊥ ≈ F) START *************)
lemma EqRelFormula_is_CopVsParIntr: ∀F,G.(F⊗G)^⊥^⊥ ≃ (F^⊥⊠G^⊥)^⊥.
  #F1 #F2 
  @EqRelFormula_is_CntNeg whd @EqFormulaLift
  @CntFormulaLift @RelFormulaNegTimes qed.  
  
lemma EqRelFormula_is_ParVsCopExtr: ∀F,G.(F^⊥⊠G^⊥)^⊥ ≃ (F^⊥^⊥⊗G^⊥^⊥).
  #F1 #F2
  whd @EqFormulaLift @CntFormulaLift @RelFormulaNegPar qed.

lemma EqRelFormula_is_ParVsCopIntr: ∀F,G.(F⊠G)^⊥^⊥ ≃ (F^⊥⊗G^⊥)^⊥.
  #F1 #F2
  @EqRelFormula_is_CntNeg whd @EqFormulaLift @CntFormulaLift
  @RelFormulaNegPar qed.

lemma EqRelFormula_is_CopVsParExtr: ∀F,G.(F^⊥⊗G^⊥)^⊥ ≃ (F^⊥^⊥⊠G^⊥^⊥).
  #F1 #F2
  whd @EqFormulaLift @CntFormulaLift @RelFormulaNegTimes qed.

lemma EqRelFormula_is_dual_if: ∀F. F^⊥^⊥ ≃ F → (∃G. G^⊥ ≃ F).
  #F1 #EqRel % [ @(F1^⊥)] assumption qed.

lemma EqRelFormula_is_dual_onlyif: ∀F.(∃G.G^⊥ ≃ F) → F^⊥^⊥ ≃ F.
  #F1 #E elim F1
  [1:
  @(EqRelFormula_is_Tran ? 𝟙^⊥ ?)
    [@(EqRelFormula_is_CntNeg 𝟙^⊥ 𝟙) ] @(EqFormulaLift 𝟙^⊥ ?) /2/
  |2: #N @(EqRelFormula_is_Tran ?  ((𝔹 \sub N)^⊥) ?) 
    [ @EqRelFormula_is_CntNeg @EqRelFormula_is_Sym] @EqFormulaLift @CntFormulaLift /2/       
  |3: #N @(EqRelFormula_is_Tran ?  ((𝔸 \sub N)^⊥) ?)
    [ @EqRelFormula_is_CntNeg @EqRelFormula_is_Sym ] @EqFormulaLift @CntFormulaLift /2/
  |4:  #F2 #EqRel @EqRelFormula_is_CntNeg assumption
  |5: #F2 #F3 #EqRel1 #EqRel2 @(EqRelFormula_is_Tran ?  (F2^⊥⊠F3^⊥)^⊥ ? ) 
    [  @EqRelFormula_is_CopVsParIntr
      | @(EqRelFormula_is_Tran ? (F2^⊥^⊥⊗F3^⊥^⊥) ?) // 
       @(EqRelFormula_is_CntCopLR F2^⊥^⊥ F2 F3^⊥^⊥ F3) assumption]
  | #F2 #F3 #EqRel1 #EqRel2  @(EqRelFormula_is_Tran ? (F2^⊥⊗F3^⊥)^⊥ ? )
    [ @EqRelFormula_is_ParVsCopIntr
      | @(EqRelFormula_is_Tran ?  (F2^⊥^⊥⊠F3^⊥^⊥) ?)
        [  @EqRelFormula_is_CopVsParExtr 
          | @(EqRelFormula_is_CntParLR F2^⊥^⊥ F2 F3^⊥^⊥ F3) assumption qed.

(******  F^⊥^⊥ ≈ F ⇔ (∃G.G^⊥ ≈ F) STOP **************)

lemma test: 𝟙 ≃ (𝟙 ⊠ 𝟙^⊥).
  @(EqFormulaTran ? (𝟙⊠𝟙) ?) @EqFormulaLift;
  [2: @(CntFormulaParR ? ? ?) ] @CntFormulaLift /2/ qed.

lemma Times_is_Assoc: ∀ F,G,H. (F⊗(G⊗H)) ≃ (F⊗G⊗H).
  #F1 #F2 #F3 whd @EqFormulaLift @CntFormulaLift @RelFormulaCopAsc qed.


lemma Times_is_Symm: ∀ F,G. (F⊗G) ≃ (G⊗F).
  #F1 #F2 whd @EqFormulaLift @CntFormulaLift @RelFormulaCopSym qed.

lemma Times_has_Unit: ∀ F. (𝟙⊗F) ≃ F. 
  #F1 whd @EqFormulaLift @CntFormulaLift @RelFormulaCopUnit qed.


lemma NotNotR_eq_R: ∀ F. F^⊥^⊥ ≃ F .
  #F1 elim F1
 [1: @(EqRelFormula_is_dual_onlyif 𝟙); 
    % [ @𝟙 | whd; @EqFormulaLift @CntFormulaLift // ]
 |2: #N @(EqRelFormula_is_dual_onlyif 𝔸\sub N); 
    % [ @ (𝔹\sub N) | whd; @EqFormulaLift @CntFormulaLift //]
 |3: #N @(EqRelFormula_is_dual_onlyif 𝔹\sub N) 
    % [ @(𝔸\sub N)  | whd; @EqFormulaLift @CntFormulaLift //]
 |4: #F2 #EqRel  @EqRelFormula_is_CntNeg assumption
 |5: #F2 #F3 #EqRel1 #EqRel2 @(EqRelFormula_is_dual_onlyif (F2⊗F3))
    % [ @(F2^⊥⊠F3^⊥) | @(EqRelFormula_is_Tran ? (F2^⊥^⊥⊗F3^⊥^⊥) ?);
        [ @EqRelFormula_is_ParVsCopExtr @EqRelFormula_is_CntCopLR ] /2/ ]
 |6: #F2 #F3 #EqRel1 #EqRel2 @(EqRelFormula_is_dual_onlyif (F2⊠F3));
    % [ @(F2^⊥⊗F3^⊥)| @(EqRelFormula_is_Tran ? (F2^⊥^⊥⊠F3^⊥^⊥) ?)
        [ @EqRelFormula_is_CopVsParExtr | @EqRelFormula_is_CntParLR ] //]
 ] qed.

lemma Formula_is_CntNegInv: ∀F,G.F^⊥ ≃ G^⊥ → F ≃ G.
  #F1 #F2 #EqRel @(EqRelFormula_is_Tran ? F1^⊥^⊥ ?)
  [1: @(EqRelFormula_is_Sym ??) @NotNotR_eq_R
  |2: @(EqRelFormula_is_Tran ? F2^⊥^⊥ ?)
    [1: @EqRelFormula_is_CntNeg assumption 
    |2: @NotNotR_eq_R
    ]
  ] qed.


(******** Structures and relative morphisms START ***********)
definition Structure: setoid .
 % 1
 [1: @Formula
 |2: @EqRelFormula
 ] qed.

definition NegMorph: Structure ⇒ Structure.
 % 1; 
  [1: @Neg
  |2: #S1 #S2 #Eq @EqRelFormula_is_CntNeg;
    assumption 
  ]
qed.

interpretation "NegMorph" 
   'Neg a = (NegMorph a).

definition TensorMorph: Structure × Structure ⇒ Structure.
 % 1; 
  [ @Times
  | #S1 #S2 #S3 #S4 #Eq1 #Eq2  @EqRelFormula_is_CntCopLR assumption
  ]
qed.

interpretation "TensorMorph" 
  'Tensor a b = (TensorMorph a b).

definition ParMorph: Structure × Structure ⇒ Structure.
 % 1;
  [ @Par
  | #S1 #S2 #S3 #S4 #Eq1 #Eq2 @EqRelFormula_is_CntParLR assumption
  ]
qed.

interpretation "ParMorph" 
  'Par a b = (ParMorph a b).
(******** Structures and relative morphisms STOP ***********)
